Nuprl Lemma : ifthenelse_wf
12,41
postcript
pdf
b
:
,
A
:Type,
p
,
q
:
A
. if
b
then
p
else
q
fi
A
latex
ProofTree
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
if
b
then
t
else
f
fi
,
Lemmas
bool
wf
origin
b:
, A:Type, p, q:A. if b then p else q fi 
A
b:, A:Type, p, q:A. if b then p else q fi A
Tx:A. B(x)